Add kani proofs

.devcontainer.json

@@ -0,0 +1,3 @@
+{
+  "image": "ghcr.io/bootc-dev/devenv-debian:latest"
+}

.github/workflows/build.yml

@@ -1,34 +1,42 @@
-name: Rust
+name: CI
+
 on:
   push:
     branches: [main]
   pull_request:
     branches: [main]
+
 permissions:
   contents: read
 
-# don't waste job slots on superseded code
+# Don't waste job slots on superseded code
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
-env:
-  CARGO_TERM_COLOR: always
-
 jobs:
-  tests-stable:
-    name: Tests, stable toolchain
+  ci:
+    name: CI
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Build and run CI in devcontainer
+        uses: devcontainers/ci@v0.3
+        with:
+          push: never
+          runCmd: just ci
+
+  kani:
+    name: Kani formal verification
     runs-on: ubuntu-latest
     steps:
-      - name: Check out repository
+      - name: Checkout
         uses: actions/checkout@v4
-      - name: Install toolchain
-        uses: dtolnay/rust-toolchain@v1
+
+      - name: Run Kani proofs in devcontainer
+        uses: devcontainers/ci@v0.3
         with:
-          toolchain: stable
-      - name: Cache build artifacts
-        uses: Swatinem/rust-cache@v2
-      - name: cargo build
-        run: cargo build --all-targets
-      - name: cargo test
-        run: cargo test --all-targets
+          push: never
+          runCmd: just kani

Cargo.toml

@@ -7,6 +7,9 @@ authors = ["Colin Walters <walters@verbum.org>"]
 license = "MIT OR Apache-2.0"
 repository = "https://github.com/cgwalters/spec-json-rpc-fdpass"
 
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
 [dependencies]
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
@@ -20,3 +23,4 @@ jsonrpsee = { version = "0.24", features = ["server", "client-core", "async-clie
 [dev-dependencies]
 tempfile = "3.0"
 async-trait = "0.1"
+kani-verifier = "0.67"

Justfile

@@ -0,0 +1,58 @@
+# Format, lint, and type-check
+check:
+	cargo fmt --check
+	cargo clippy --all-targets
+	cargo check --all-targets
+
+# Auto-format code
+fmt:
+	cargo fmt
+
+# Run unit tests (uses nextest if available)
+unit:
+	@if cargo nextest --version >/dev/null 2>&1; then \
+		cargo nextest run; \
+	else \
+		cargo test; \
+	fi
+
+# Run all tests
+test-all: unit
+
+# Build release binaries
+build:
+	cargo build --release
+
+# Build debug binaries
+build-debug:
+	cargo build
+
+# Generate docs
+doc:
+	cargo doc --no-deps
+
+# Open docs in browser
+doc-open:
+	cargo doc --no-deps --open
+
+# Clean build artifacts
+clean:
+	cargo clean
+
+# Full CI check (format, lint, test)
+ci: check unit
+
+# Run Kani formal verification proofs
+# NOTE: Kani requires rustup (won't work with distro-packaged Rust)
+# Install: cargo install --locked kani-verifier && cargo kani setup
+# Alternatively, Kani proofs run automatically in CI via GitHub Actions
+kani:
+	cargo kani
+
+# Run a specific Kani proof by name
+kani-proof name:
+	cargo kani --harness {{name}}
+
+# List available Kani proofs
+kani-list:
+	cargo kani --list

src/message.rs

@@ -20,7 +20,7 @@ pub fn get_fd_count(value: &serde_json::Value) -> usize {
 
 /// Helper to skip serializing fds field when it's None or 0
 fn skip_if_zero_or_none(fds: &Option<usize>) -> bool {
-    fds.map_or(true, |n| n == 0)
+    fds.is_none_or(|n| n == 0)
 }
 
 /// A JSON-RPC 2.0 request message.
@@ -256,3 +256,66 @@ pub fn file_descriptor_error() -> JsonRpcError<'static> {
         None::<serde_json::Value>,
     )
 }
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    // =========================================================================
+    // Proofs for skip_if_zero_or_none
+    // =========================================================================
+
+    /// Verify that skip_if_zero_or_none returns true for None
+    #[kani::proof]
+    fn check_skip_none() {
+        let result = skip_if_zero_or_none(&None);
+        kani::assert(result, "None should be skipped");
+    }
+
+    /// Verify that skip_if_zero_or_none returns true for Some(0)
+    #[kani::proof]
+    fn check_skip_zero() {
+        let result = skip_if_zero_or_none(&Some(0));
+        kani::assert(result, "Some(0) should be skipped");
+    }
+
+    /// Verify that skip_if_zero_or_none returns false for any non-zero value
+    #[kani::proof]
+    fn check_skip_nonzero() {
+        let n: usize = kani::any();
+        kani::assume(n > 0);
+        let result = skip_if_zero_or_none(&Some(n));
+        kani::assert(!result, "Some(n > 0) should not be skipped");
+    }
+
+    // =========================================================================
+    // Proofs for JsonRpcMessage::get_fds
+    // =========================================================================
+
+    /// Verify get_fds returns 0 when fds field is None
+    #[kani::proof]
+    fn check_get_fds_none() {
+        let msg = JsonRpcMessage::Notification(JsonRpcNotification {
+            jsonrpc: String::new(),
+            method: String::new(),
+            params: None,
+            fds: None,
+        });
+        let result = msg.get_fds();
+        kani::assert(result == 0, "None fds should return 0");
+    }
+
+    /// Verify get_fds returns the value when fds field is Some(n)
+    #[kani::proof]
+    fn check_get_fds_some() {
+        let n: usize = kani::any();
+        let msg = JsonRpcMessage::Notification(JsonRpcNotification {
+            jsonrpc: String::new(),
+            method: String::new(),
+            params: None,
+            fds: Some(n),
+        });
+        let result = msg.get_fds();
+        kani::assert(result == n, "get_fds should return the fds value");
+    }
+}

src/transport.rs

@@ -1,11 +1,11 @@
 use crate::error::{Error, Result};
 use crate::message::{get_fd_count, JsonRpcMessage, JsonRpcNotification, MessageWithFds};
 use rustix::fd::AsFd;
-use serde::Serialize;
 use rustix::net::{
     RecvAncillaryBuffer, RecvAncillaryMessage, RecvFlags, SendAncillaryBuffer,
     SendAncillaryMessage, SendFlags,
 };
+use serde::Serialize;
 use std::collections::VecDeque;
 use std::io::{self, IoSlice, IoSliceMut};
 use std::num::NonZeroUsize;
@@ -148,7 +148,9 @@ impl Sender {
             let remaining_fds = &fds[fds_sent..];
 
             // Determine how many FDs to send in this batch (up to current_max_fds)
-            let fds_batch = remaining_fds.get(..current_max_fds).unwrap_or(remaining_fds);
+            let fds_batch = remaining_fds
+                .get(..current_max_fds)
+                .unwrap_or(remaining_fds);
 
             let result = self
                 .stream

tests/integration_tests.rs

@@ -195,9 +195,9 @@ async fn test_multiple_messages_with_fds_sequential() -> Result<()> {
 
     // Create multiple test files with different content
     let mut temp_files = Vec::new();
-    let test_contents = vec!["Content 1", "Content 2", "Content 3"];
+    let test_contents = ["Content 1", "Content 2", "Content 3"];
 
-    for (_i, content) in test_contents.iter().enumerate() {
+    for content in test_contents.iter() {
         let mut temp_file = NamedTempFile::new().unwrap();
         write!(temp_file, "{}", content).unwrap();
         temp_file.flush().unwrap();
@@ -1932,7 +1932,10 @@ async fn test_fd_batching_one_per_message() -> Result<()> {
                 assert_eq!(contents.trim(), expected, "FD {} has wrong content", i);
             }
 
-            Ok((Some(Value::String("All FDs verified".to_string())), Vec::new()))
+            Ok((
+                Some(Value::String("All FDs verified".to_string())),
+                Vec::new(),
+            ))
         });
 
         if let Ok((stream, _)) = listener.accept().await {
@@ -2105,13 +2108,18 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> {
             tf.flush().unwrap();
             temp_files.push(tf);
         }
-        let fds: Vec<OwnedFd> = temp_files.into_iter().map(|tf| tf.into_file().into()).collect();
+        let fds: Vec<OwnedFd> = temp_files
+            .into_iter()
+            .map(|tf| tf.into_file().into())
+            .collect();
         let request = JsonRpcRequest::new(
             "with_fds".to_string(),
             Some(serde_json::json!({ "expected_fds": 3 })),
             Value::Number(1.into()),
         );
-        sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)).await?;
+        sender
+            .send(MessageWithFds::new(JsonRpcMessage::Request(request), fds))
+            .await?;
     }
 
     // Message 2: No FDs
@@ -2121,7 +2129,12 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> {
             Some(serde_json::json!({ "check": "first" })),
             Value::Number(2.into()),
         );
-        sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), vec![])).await?;
+        sender
+            .send(MessageWithFds::new(
+                JsonRpcMessage::Request(request),
+                vec![],
+            ))
+            .await?;
     }
 
     // Message 3: 2 FDs
@@ -2133,13 +2146,18 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> {
             tf.flush().unwrap();
             temp_files.push(tf);
         }
-        let fds: Vec<OwnedFd> = temp_files.into_iter().map(|tf| tf.into_file().into()).collect();
+        let fds: Vec<OwnedFd> = temp_files
+            .into_iter()
+            .map(|tf| tf.into_file().into())
+            .collect();
         let request = JsonRpcRequest::new(
             "with_fds".to_string(),
             Some(serde_json::json!({ "expected_fds": 2 })),
             Value::Number(3.into()),
         );
-        sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)).await?;
+        sender
+            .send(MessageWithFds::new(JsonRpcMessage::Request(request), fds))
+            .await?;
     }
 
     // Message 4: No FDs
@@ -2149,7 +2167,12 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> {
             Some(serde_json::json!({ "check": "second" })),
             Value::Number(4.into()),
         );
-        sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), vec![])).await?;
+        sender
+            .send(MessageWithFds::new(
+                JsonRpcMessage::Request(request),
+                vec![],
+            ))
+            .await?;
     }
 
     // Message 5: 4 FDs
@@ -2161,13 +2184,18 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> {
             tf.flush().unwrap();
             temp_files.push(tf);
         }
-        let fds: Vec<OwnedFd> = temp_files.into_iter().map(|tf| tf.into_file().into()).collect();
+        let fds: Vec<OwnedFd> = temp_files
+            .into_iter()
+            .map(|tf| tf.into_file().into())
+            .collect();
         let request = JsonRpcRequest::new(
             "with_fds".to_string(),
             Some(serde_json::json!({ "expected_fds": 4 })),
             Value::Number(5.into()),
         );
-        sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)).await?;
+        sender
+            .send(MessageWithFds::new(JsonRpcMessage::Request(request), fds))
+            .await?;
     }
 
     server_handle.abort();