Enrich unit tests with symbolic proofs

.github/workflows/verify.yaml

@@ -0,0 +1,26 @@
+name: Verification
+on:
+  pull_request:
+  merge_group:
+
+jobs:
+  verify-wire:
+    runs-on: [macos-latest]
+    steps:
+      - name: 'Checkout your code.'
+        uses: actions/checkout@v3
+
+      - name: 'Run Kani on TCP wire.'
+        uses: model-checking/[email protected]
+        with:
+          args: '--output-format=terse --verbose --harness wire::tcp::verification'
+  verify-socket:
+    runs-on: [macos-latest]
+    steps:
+      - name: 'Checkout your code.'
+        uses: actions/checkout@v3
+
+      - name: 'Run Kani on TCP socket.'
+        uses: model-checking/[email protected]
+        with:
+          args: '--output-format=terse --verbose --harness socket::tcp::verification'

src/iface/interface/mod.rs

@@ -968,7 +968,7 @@ impl InterfaceInner {
         None
     }
 
-    #[cfg(test)]
+    #[cfg(any(test, kani))]
     #[allow(unused)] // unused depending on which sockets are enabled
     pub(crate) fn set_now(&mut self, now: Instant) {
         self.now = now

src/lib.rs

@@ -129,7 +129,7 @@ mod macros;
 mod parsers;
 mod rand;
 
-#[cfg(test)]
+#[cfg(any(test, kani))]
 mod config {
     #![allow(unused)]
     pub const ASSEMBLER_MAX_SEGMENT_COUNT: usize = 4;
@@ -149,7 +149,7 @@ mod config {
     pub const IPV6_HBH_MAX_OPTIONS: usize = 2;
 }
 
-#[cfg(not(test))]
+#[cfg(not(any(test, kani)))]
 mod config {
     #![allow(unused)]
     include!(concat!(env!("OUT_DIR"), "/config.rs"));
@@ -170,7 +170,7 @@ pub mod time;
 pub mod wire;
 
 #[cfg(all(
-    test,
+    any(test, kani),
     any(
         feature = "medium-ethernet",
         feature = "medium-ip",