Add Github actions and some initial build files.

PiperOrigin-RevId: 687389500

.bazelrc

@@ -0,0 +1,3 @@
+# Use C++ 20.
+build --cxxopt=-std=c++20
+build --host_cxxopt=-std=c++20

.github/workflows/ci.yml

@@ -0,0 +1,48 @@
+name: build
+
+# Controls when the workflow will run
+on:
+  # Triggers the workflow on push or pull request events but only for the "main" branch
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+  schedule:
+    # Run daily at midnight to ensure we catch regressions.
+    - cron: "0 0 * * *"
+  # Manual
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Mount bazel cache
+        uses: actions/cache/restore@v4
+        with:
+          path: "~/.cache/bazel"
+          key: bazel-${{ hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}-${{ github.ref_name }}
+          restore-keys: |
+            bazel-${{hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}-${{ github.ref_name }}
+            bazel-${{hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}
+            bazel-
+
+
+      - name: Build
+        run: ./bazel build --test_output=errors //...
+      - name: Test
+        run: ./bazel test --test_output=errors //...
+
+      - name: Compress cache
+        run: rm -rf $(./bazel info repository_cache)
+
+      - name: Save bazel cache
+        uses: actions/cache/save@v4
+        # Only create a new cache entry if we're on the main branch or the build takes >5mins.
+        if: github.ref_name == "main" || env.duration > 300
+        with:
+          path: "~/.cache/bazel"
+          key: bazel-${{ hashFiles('MODULE.bazel', 'WORKSPACE.bazel', '.bazelrc') }}-${{ github.ref_name }}-${{ github.run_id }}

BUILD → BUILD.bazel

@@ -1,8 +1,11 @@
 # NetKAT, a framework for describing and reasoning about packet-switched networks.
 
-load("//tools/build_defs/license:license.bzl", "license")
+load("@rules_license//rules:license.bzl", "license")
 
-package(default_applicable_licenses = [":license"])
+package(
+    default_applicable_licenses = [":license"],
+    default_visibility = [":__subpackages__"],
+)
 
 # Define the license for this package, which is used as the default license
 # for all targets in this package based on default_applicable_licenses above.

MODULE.bazel

@@ -0,0 +1,28 @@
+# Copyright 2024 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.
+
+# https://bazel.build/external/overview#bzlmod
+
+module(
+    name = "google-netkat",
+    version = "0.0.1",
+    bazel_compatibility = [">=7.3.2"],
+    compatibility_level = 1,
+)
+
+bazel_dep(name = "rules_cc", version = "0.0.13")
+bazel_dep(name = "rules_license", version = "1.0.0")
+bazel_dep(name = "protobuf", version = "28.2", repo_name = "com_google_protobuf")
+bazel_dep(name = "abseil-cpp", version = "20240116.2", repo_name = "com_google_absl")
+bazel_dep(name = "googletest", version = "1.15.2", repo_name = "com_google_googletest")

README.md

@@ -5,37 +5,37 @@ This is a C++ implementation of NetKAT.
 NetKAT is a domain specific language (DSL) and system for specifying,
 programming, and reasoning about packet-switched networks. Key features include:
 
-* Automated reasoning and verification.
-* Modular composition, supporting clean isolation and abstraction.
-* Simple, yet very powerful syntax & semantics.
-* Strong mathematical foundation.
+*   Automated reasoning and verification.
+*   Modular composition, supporting clean isolation and abstraction.
+*   Simple, yet very powerful syntax & semantics.
+*   Strong mathematical foundation.
 
 If you want to learn more, you may check out the list of
-[publications on NetKAT](#academic-publications-on-netkat) below. In the future,
+[pulbications on NetKAT](#academic-publications-on-netkat) below. In the future,
 we also hope to provide a gentler introduction to NetKAT in the form of a
 tutorial.
 
-Note: We expect that this NetKAT implementation may diverge from NeKAT as
-described [in the literature](#academic-publications-on-netkat) over time,
-as we take liberty to optimize and adjust the language for industrial use.
+Note: We expect that this NetKAT implementation may diverge from NetKAT as
+described [in the literature](#academic-publications-on-netkat) over time, as we
+take liberty to optimize and adjust the language for industrial use.
 
 ## Disclaimer
 
-This is not an officially supported Google product. This project is not
-eligible for the [Google Open Source Software Vulnerability Rewards
-Program](https://bughunters.google.com/open-source-security).
+This is not an officially supported Google product. This project is not eligible
+for the
+[Google Open Source Software Vulnerability Rewards Program](https://bughunters.google.com/open-source-security).
 
 ## Academic Publications on NetKAT
 
-NetKAT was first conceived and studied in academia.
-Here, we list a small selection of key publications related to NetKAT.
+NetKAT was first conceived and studied in academia. Here, we list a small
+selection of key publications related to NetKAT.
 
-* **NetKAT: Semantic Foundations for Networks.** POPL 2014.
-  [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/frenetic-netkat.pdf)
-* **A Fast Compiler for NetKAT.** ICFP 2015.
-  [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/netkat-compiler.pdf)
-* **KATch: A Fast Symbolic Verifier for NetKAT.** PLDI 2024.
-  [[PDF]](https://research.google/pubs/katch-a-fast-symbolic-verifier-for-netkat/)
+*   **NetKAT: Semantic Foundations for Networks.** POPL 2014.
+    [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/frenetic-netkat.pdf)
+*   **A Fast Compiler for NetKAT.** ICFP 2015.
+    [[PDF]](https://www.cs.cornell.edu/~jnfoster/papers/netkat-compiler.pdf)
+*   **KATch: A Fast Symbolic Verifier for NetKAT.** PLDI 2024.
+    [[PDF]](https://research.google/pubs/katch-a-fast-symbolic-verifier-for-netkat/)
 
 ## Contributing
 
@@ -49,22 +49,22 @@ information.
 
 Apache header:
 
-    Copyright 2024 Google LLC
+```
+Copyright 2024 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
+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
+    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.
+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.
+```
 
 This can be done automatically using
-[addlicense](https://github.com/google/addlicense) as follows:
-```sh
-addlicense -c "The NetKAT Authors" -l apache ./netkat
-```
+[addlicense](https://github.com/google/addlicense) as follows: `sh addlicense -c
+"The NetKAT authors" -l apache .`

docs/CONTRIBUTING.md

@@ -20,8 +20,8 @@ sign a new one.
 
 ### Review our Community Guidelines
 
-This project follows [Google's Open Source Community
-Guidelines](https://opensource.google/conduct/).
+This project follows
+[Google's Open Source Community Guidelines](https://opensource.google/conduct/).
 
 ## Contribution process
 

netkat/BUILD.bazel

@@ -0,0 +1,26 @@
+
+
+package(
+    default_applicable_licenses = ["//:license"],
+    default_visibility = [":__subpackages__"],
+)
+
+proto_library(
+    name = "netkat_proto",
+    srcs = ["netkat.proto"],
+)
+
+cc_proto_library(
+    name = "netkat_cc_proto",
+    deps = [":netkat_proto"],
+)
+
+cc_test(
+    name = "netkat_test",
+    srcs = ["netkat_test.cc"],
+    deps = [
+        ":netkat_cc_proto",
+        "@com_google_absl//absl/log",
+        "@com_google_googletest//:gtest_main",
+    ],
+)

netkat/netkat.proto

@@ -0,0 +1,88 @@
+// Copyright 2024 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.
+// -----------------------------------------------------------------------------
+
+// Proto representation of NetKAT programs (predicates and policies).
+//
+// This representation is NOT intended as a user-facing API. Instead, it serves
+// as an intermdiate representation (IR) that is produced by user-facing
+// NetKAT APIs (NetKAT frontend(s)) and consumed by NetKAT backends.
+//
+// This reprensentation is expected to lack the convenience and type safety of
+// the user-facing API.
+//
+// Why have an IR?
+// * Designing an ergonomic user-facing API is hard, and requires resolving many
+//   design questions without an obvious "best" answer.
+// * By having an IR, we can immediately work on the backend without waiting for
+//   the user-facing API to be finalized. More generally, it decouples the
+//   frontend design from the backend design.
+// * Given that there is likely not a single best user-facing API, we may want
+//   to explore multiple ones (but share the IR and backend).
+// * It may make sense to have a specialized frontend API tailroed to Google's
+//   internal needs, but it will likely not be open-sourceable.
+//
+// Why use protobufs for the IR?
+// * It provides many useful features out of the box:
+//   serialization/deserialization, pretty-printing, a text format, fuzzing
+//   (e.g. using https://github.com/google/fuzztest), diffing.
+// * It makes it easy to implement frontends and backends in different
+//   programming languages.
+// * It makes it easy to run backends as (gRPC) services.
+
+syntax = "proto3";
+
+package netkat;
+
+// A NetKAT predicate (internal intermdiate representation).
+message PredicateProto {
+  oneof predicate {
+    Bool bool_constant = 1;
+    Match match = 3;
+    And and_operation = 4;
+    Or or_operation = 5;
+    Not not_operation = 6;
+  }
+
+  // A boolean constant (true or false).
+  message Bool {
+    bool value = 1;
+  }
+
+  // Checks if a field has a specific value.
+  //
+  // NOTE: This message is expected to change in the future! E.g., the type of
+  // `value` will change to support things like 128-bit IPv6 addresses.
+  message Match {
+    string field = 1;
+    int32 value = 2;
+  }
+
+  // Boolean conjunction (&&) of two predicates.
+  message And {
+    PredicateProto left = 1;
+    PredicateProto right = 2;
+  }
+
+  // Boolean disjunction (||) of two predicates.
+  message Or {
+    PredicateProto left = 1;
+    PredicateProto right = 2;
+  }
+
+  // Boolean negation (!) of a predicate.
+  message Not {
+    PredicateProto negand = 1;
+  }
+}