From 9aaf707ea8709f1e087b9109a7df3b7193f36f43 Mon Sep 17 00:00:00 2001 From: Colin Walters Date: Mon, 26 Jan 2026 13:24:02 -0500 Subject: [PATCH 1/5] lib: Apply clippy suggestions Use is_none_or instead of map_or for clarity, reformat code. Assisted-by: OpenCode (Claude Sonnet 4) --- src/message.rs | 2 +- src/transport.rs | 6 +++-- tests/integration_tests.rs | 50 +++++++++++++++++++++++++++++--------- 3 files changed, 44 insertions(+), 14 deletions(-) diff --git a/src/message.rs b/src/message.rs index 75d784b..ff02d77 100644 --- a/src/message.rs +++ b/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) -> bool { - fds.map_or(true, |n| n == 0) + fds.is_none_or(|n| n == 0) } /// A JSON-RPC 2.0 request message. diff --git a/src/transport.rs b/src/transport.rs index 66ed8c3..26dcb6c 100644 --- a/src/transport.rs +++ b/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 diff --git a/tests/integration_tests.rs b/tests/integration_tests.rs index cf13fa1..4a82763 100644 --- a/tests/integration_tests.rs +++ b/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 = temp_files.into_iter().map(|tf| tf.into_file().into()).collect(); + let fds: Vec = 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 = temp_files.into_iter().map(|tf| tf.into_file().into()).collect(); + let fds: Vec = 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 = temp_files.into_iter().map(|tf| tf.into_file().into()).collect(); + let fds: Vec = 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(); From edcbb784038fe7eda375936107140a1b74473c57 Mon Sep 17 00:00:00 2001 From: Colin Walters Date: Mon, 26 Jan 2026 13:24:13 -0500 Subject: [PATCH 2/5] lib: Add Kani formal verification proofs Add bounded model checking proofs using Kani to verify key invariants: - skip_if_zero_or_none: correctly identifies values to skip serializing - set_fds/get_fds: round-trip property holds for all message types - get_fds: returns 0 when fds field is None Also adds: - GitHub Actions workflow job to run Kani proofs in CI - Justfile with common development commands including kani targets Kani is a bounded model checker that mathematically proves these properties hold for all possible inputs within bounds, providing stronger guarantees than traditional testing. Assisted-by: OpenCode (Claude Sonnet 4) --- .github/workflows/build.yml | 9 +++++ Cargo.toml | 4 ++ Justfile | 58 +++++++++++++++++++++++++++ src/message.rs | 80 +++++++++++++++++++++++++++++++++++++ 4 files changed, 151 insertions(+) create mode 100644 Justfile diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index b08f714..e3c60d0 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -32,3 +32,12 @@ jobs: run: cargo build --all-targets - name: cargo test run: cargo test --all-targets + + kani: + name: Kani formal verification + runs-on: ubuntu-latest + steps: + - name: Check out repository + uses: actions/checkout@v4 + - name: Run Kani proofs + uses: model-checking/kani-github-action@v1 diff --git a/Cargo.toml b/Cargo.toml index 27b356e..8a7aab4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,6 +7,9 @@ authors = ["Colin Walters "] 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" diff --git a/Justfile b/Justfile new file mode 100644 index 0000000..c41dee3 --- /dev/null +++ b/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 diff --git a/src/message.rs b/src/message.rs index ff02d77..b7098ff 100644 --- a/src/message.rs +++ b/src/message.rs @@ -256,3 +256,83 @@ pub fn file_descriptor_error() -> JsonRpcError<'static> { None::, ) } + +#[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::set_fds / get_fds round-trip + // ========================================================================= + + /// Verify that set_fds(n) followed by get_fds() returns n for requests + #[kani::proof] + fn check_set_get_fds_request() { + let count: usize = kani::any(); + let mut msg = JsonRpcMessage::Request(JsonRpcRequest { + jsonrpc: String::new(), + method: String::new(), + params: None, + id: serde_json::Value::Null, + fds: None, + }); + msg.set_fds(count); + let result = msg.get_fds(); + kani::assert(result == count, "get_fds should return what set_fds set"); + } + + /// Verify that set_fds(0) results in get_fds() returning 0 + #[kani::proof] + fn check_set_zero_fds() { + let mut msg = JsonRpcMessage::Response(JsonRpcResponse { + jsonrpc: String::new(), + result: None, + error: None, + id: serde_json::Value::Null, + fds: Some(42), // Start with non-zero + }); + msg.set_fds(0); + let result = msg.get_fds(); + kani::assert(result == 0, "set_fds(0) should clear 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"); + } +} From 47911ccde4fb9b2b62655af4c0a37a5676e75245 Mon Sep 17 00:00:00 2001 From: Colin Walters Date: Mon, 26 Jan 2026 13:24:16 -0500 Subject: [PATCH 3/5] Add basic devcontainer configuration Points to Microsoft's Rust devcontainer image for VS Code/Codespaces. Assisted-by: OpenCode (Claude Sonnet 4) --- .devcontainer.json | 1 + 1 file changed, 1 insertion(+) create mode 100644 .devcontainer.json diff --git a/.devcontainer.json b/.devcontainer.json new file mode 100644 index 0000000..a09eb8d --- /dev/null +++ b/.devcontainer.json @@ -0,0 +1 @@ +{"image":"mcr.microsoft.com/devcontainers/rust:latest"} \ No newline at end of file From b4187a2148af5a37a619dbcdc6b61662527b2b56 Mon Sep 17 00:00:00 2001 From: Colin Walters Date: Mon, 26 Jan 2026 22:04:59 -0500 Subject: [PATCH 4/5] kani: Simplify proofs to avoid serde_json state explosion The proofs using JsonRpcRequest/Response with kani::any() caused combinatorial explosion in Kani's bounded model checking due to the complexity of serde_json::Value types. Simplify to focus on verifiable properties: - skip_if_zero_or_none: 3 proofs covering None, Some(0), Some(n>0) - get_fds: 2 proofs covering None and Some(n) cases These 5 proofs now complete successfully in ~0.02s each. Assisted-by: OpenCode (Claude Sonnet 4) --- src/message.rs | 37 ++++++++++--------------------------- 1 file changed, 10 insertions(+), 27 deletions(-) diff --git a/src/message.rs b/src/message.rs index b7098ff..79ca24e 100644 --- a/src/message.rs +++ b/src/message.rs @@ -289,50 +289,33 @@ mod verification { } // ========================================================================= - // Proofs for JsonRpcMessage::set_fds / get_fds round-trip + // Proofs for JsonRpcMessage::get_fds // ========================================================================= - /// Verify that set_fds(n) followed by get_fds() returns n for requests + /// Verify get_fds returns 0 when fds field is None #[kani::proof] - fn check_set_get_fds_request() { - let count: usize = kani::any(); - let mut msg = JsonRpcMessage::Request(JsonRpcRequest { + fn check_get_fds_none() { + let msg = JsonRpcMessage::Notification(JsonRpcNotification { jsonrpc: String::new(), method: String::new(), params: None, - id: serde_json::Value::Null, fds: None, }); - msg.set_fds(count); let result = msg.get_fds(); - kani::assert(result == count, "get_fds should return what set_fds set"); - } - - /// Verify that set_fds(0) results in get_fds() returning 0 - #[kani::proof] - fn check_set_zero_fds() { - let mut msg = JsonRpcMessage::Response(JsonRpcResponse { - jsonrpc: String::new(), - result: None, - error: None, - id: serde_json::Value::Null, - fds: Some(42), // Start with non-zero - }); - msg.set_fds(0); - let result = msg.get_fds(); - kani::assert(result == 0, "set_fds(0) should clear fds"); + kani::assert(result == 0, "None fds should return 0"); } - /// Verify get_fds returns 0 when fds field is None + /// Verify get_fds returns the value when fds field is Some(n) #[kani::proof] - fn check_get_fds_none() { + fn check_get_fds_some() { + let n: usize = kani::any(); let msg = JsonRpcMessage::Notification(JsonRpcNotification { jsonrpc: String::new(), method: String::new(), params: None, - fds: None, + fds: Some(n), }); let result = msg.get_fds(); - kani::assert(result == 0, "None fds should return 0"); + kani::assert(result == n, "get_fds should return the fds value"); } } From 6eb61ab1638f2ce06c00bbbeba9ad90c55a88290 Mon Sep 17 00:00:00 2001 From: Colin Walters Date: Tue, 27 Jan 2026 07:44:20 -0500 Subject: [PATCH 5/5] ci: Use devcontainer for CI to match local development Replace separate toolchain installation with devcontainers/ci action that runs inside the same devcontainer image used for local development. This ensures CI and local builds use identical environments. Both jobs now delegate to Justfile targets: - ci job: runs `just ci` (fmt check, clippy, tests) - kani job: runs `just kani` (formal verification proofs) Also updates .devcontainer.json to use bootc-dev/devenv-debian image which includes Kani, cargo-nextest, and other development tools. Assisted-by: OpenCode (Claude Sonnet 4) --- .devcontainer.json | 4 +++- .github/workflows/build.yml | 39 ++++++++++++++++++------------------- 2 files changed, 22 insertions(+), 21 deletions(-) diff --git a/.devcontainer.json b/.devcontainer.json index a09eb8d..c6cb5a6 100644 --- a/.devcontainer.json +++ b/.devcontainer.json @@ -1 +1,3 @@ -{"image":"mcr.microsoft.com/devcontainers/rust:latest"} \ No newline at end of file +{ + "image": "ghcr.io/bootc-dev/devenv-debian:latest" +} diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index e3c60d0..5c8e2a2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,43 +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: Check out repository + - name: Checkout uses: actions/checkout@v4 - - name: Install toolchain - uses: dtolnay/rust-toolchain@v1 + + - name: Build and run CI 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 ci kani: name: Kani formal verification runs-on: ubuntu-latest steps: - - name: Check out repository + - name: Checkout uses: actions/checkout@v4 - - name: Run Kani proofs - uses: model-checking/kani-github-action@v1 + + - name: Run Kani proofs in devcontainer + uses: devcontainers/ci@v0.3 + with: + push: never + runCmd: just kani